$\forall$$a$:Id, $T$, $A$:Type, $x$:Id, $P$:($A$$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]$T$
\\[0ex]$\Rightarrow$ $A$
\\[0ex]$\Rightarrow$ AtomFree(Type;$A$)
\\[0ex]$\Rightarrow$ AtomFree(Type;$T$)
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. Dec($\exists$$v$:$T$. $P$($a$,$v$)))
\\[0ex]$\Rightarrow$ Feasible(ma{-}single{-}pre1($x$;$A$;$a$;$T$;$x$,$v$.$P$($x$,$v$)))